package mac5789.hamcycle;

import static mac5789.utils.Range.range;

import java.util.ArrayList;
import java.util.List;

import mac5789.graph.Graph;
import mac5789.sat.CraftedSatProblem;
import mac5789.sat.SatProblem;
import mac5789.utils.Range;

/**
 * Converte grafos em problemas de satisfatibilidade para o problema do circuito
 * hamiltoniano
 * 
 * @author lundberg
 * 
 */
public class HamCycleToSat {

    /**
     * Baseado no grafo constrói um problema SAT que é satisfatível sse o grafo
     * possui um circuito hamiltoniano
     * 
     * @param graph
     *            graph
     * @return SatProblem
     */
    public SatProblem toSat(Graph graph) {
        CraftedSatProblem problem = new CraftedSatProblem();
        for (int vertex : this.vertexes(graph)) {
            this.vertexBelongsToPath(graph, problem, vertex);
            this.vertexDoesNotOccurTwiceOnPath(graph, problem, vertex);
        }
        for (int pathIndex : this.vertexes(graph)) {
            this.thereIsAVertexAtPathIndex(graph, problem, pathIndex);
            this.nextVertexOnPathMustHaveEdge(graph, problem, pathIndex);
        }
        problem.add(this.vertexAtPathIndex(graph, 0, 0));
        return problem;
    }

    /**
     * Adiciona cláusulas ao problema adicionando a restrição de que o vértice
     * deve aparecer ao menos uma vez no circuito hamiltoniano
     * 
     * @param graph
     *            graph
     * @param problem
     *            problem
     * @param vertex
     *            vertex
     */
    private void vertexBelongsToPath(Graph graph, CraftedSatProblem problem, int vertex) {
        List<Integer> clause = new ArrayList<Integer>();
        for (int pathIndex : this.pathIndexes(graph)) {
            clause.add(this.vertexAtPathIndex(graph, vertex, pathIndex));
        }
        problem.add(clause);
    }

    /**
     * Adiciona cláusulas ao problema adicionando a restrição de que o vértice
     * não deve aparecer duas vezes no circuito hamiltoniano
     * 
     * @param graph
     *            graph
     * @param problem
     *            problem
     * @param vertex
     *            vertex
     */
    private void vertexDoesNotOccurTwiceOnPath(Graph graph, CraftedSatProblem problem, int vertex) {
        for (int aPathIndex : this.pathIndexes(graph)) {
            for (int otherPathIndex : this.pathIndexes(graph)) {
                if (aPathIndex != otherPathIndex) {
                    problem.add(this.not(this.vertexAtPathIndex(graph, vertex, aPathIndex)), this.not(this.vertexAtPathIndex(graph, vertex, otherPathIndex)));
                }
            }
        }
    }

    /**
     * Adiciona cláusulas ao problema adicionando a restrição de que deve
     * existir ao menos um vértice no índice no circuito hamiltoniano
     * 
     * @param graph
     *            graph
     * @param problem
     *            problem
     * @param vertex
     *            vertex
     */
    private void thereIsAVertexAtPathIndex(Graph graph, CraftedSatProblem problem, int pathIndex) {
        List<Integer> clause = new ArrayList<Integer>();
        for (int vertex : this.vertexes(graph)) {
            clause.add(this.vertexAtPathIndex(graph, vertex, pathIndex));
        }
        problem.add(clause);
    }

    /**
     * Adiciona cláusulas ao problema adicionando a restrição de que vértices
     * vizinhos no caminho devem ser conectados por uma aresta no grafo.
     * 
     * @param graph
     *            graph
     * @param problem
     *            problem
     * @param vertex
     *            vertex
     */
    private void nextVertexOnPathMustHaveEdge(Graph graph, CraftedSatProblem problem, int pathIndex) {
        int nextPathIndex = (pathIndex + 1) % graph.getNVertexes();
        for (int aVertex : this.vertexes(graph)) {
            for (int otherVertex : this.vertexes(graph)) {
                if (aVertex != otherVertex && !graph.areNeighbours(aVertex, otherVertex)) {
                    problem.add(this.not(this.vertexAtPathIndex(graph, aVertex, pathIndex)), this
                            .not(this.vertexAtPathIndex(graph, otherVertex, nextPathIndex)));
                }
            }
        }
    }

    /**
     * Nega um literal
     * 
     * @param literal
     *            literal
     * @return negação do literal
     */
    private Integer not(Integer literal) {
        return -literal;
    }

    /**
     * Cria um literal que diz que o vértice está no índice dado do circuito
     * hamiltoniano do grafo.
     * 
     * @param vertex
     *            vertex
     * @param pathIndex
     *            pathIndex
     * @return
     */
    private Integer vertexAtPathIndex(Graph graph, int vertex, int pathIndex) {
        return vertex * graph.getNVertexes() + pathIndex + 1;
    }

    private Range vertexes(Graph graph) {
        return range(0, graph.getNVertexes());
    }

    private Range pathIndexes(Graph graph) {
        return range(0, graph.getNVertexes());
    }
}
